Các định lý bất toàn được ứng dụng cho các hệ thống hình thức có đủ độ phức tạp để biểu diễn phép toán cơ bản trên số tự nhiên và đồng thời có tính nhất quán và được tiên đề hóa một cách hiệu quả. Cụ thể là trong khuôn khổ của logic bậc nhất, các hệ thống hình thức cũng được gọi là các lý thuyết hình thức. Nhìn chung, một hệ thống hình thức là một công cụ để suy diễn, bao gồm một tập hợp các tiên đề cụ thể với quy tắc sử dụng các ký hiệu (hoặc quy tắc suy luận), cho phép rút ra một định lý mới từ các tiên đề. Một ví dụ là số học Peano bậc nhất, một hệ thống mà tất cả các biến được sử dụng để biểu diễn các số tự nhiên. Trong các hệ thống khác, như lý thuyết tập hợp, chỉ một vài câu của hệ thống hình thức diễn tả mệnh đề về các số tự nhiên. Các định lý bất toàn nói về khả năng chứng minh hình thức với những hệ thống này, hơn là nói về khả năng chứng minh theo cách hiểu thông thường.

Có một vài đặc tính mà một hệ thống hình thức có thể có, bao gồm sự hoàn chỉnh, sự nhất quán và sự tồn tại của sự tiên đề hóa hiệu quả. Các định lý bất toàn chỉ ra rằng một hệ thống bao gồm một số lượng số học vừa đủ không thể thỏa mãn đồng thời ba đặc tính này.

Sự tiên đề hóa hiệu quả

Một hệ thống hình thức được cho là được tiên đề hóa một cách hiệu quả (hay còn gọi là được sinh ra một cách hiệu quả) nếu như tập hợp các định lí của nó là đếm được đệ quy.

Điều đó có nghĩa là có một chương trình tính toán mà về nguyên lý có thể liệt kê danh sách tất cả các định lý của hệ thống mà không bao gồm bất kỳ mệnh đề nào không phải là định lý. Ví dụ về lý thuyết được đề ra một cách có hiệu quả là số học Peano và lý thuyết tập hợp Zermelo–Fraenkel (ZFC).

Lý thuyết được biết đến là số học chính xác bao gồm tất cả các mệnh đề đúng về số nguyên tiêu chuẩn trong ngôn ngữ của số học Peano. Lý thuyết này nhất quán, hoàn chỉnh, và bao gồm một số lượng vừa đủ các tiên đề. Tuy nhiên nó không có hệ tiên đề đếm được đệ quy vì thế không thỏa mãn giả thuyết của định lý bất toàn.

Sự hoàn chỉnh

Một tập hợp các tiên đề là hoàn chỉnh nếu như, đối với bất kỳ trường hợp nào trong ngôn ngữ của tiên đề, mệnh đề đó đó hoặc phủ định của nó là chứng minh được bằng các tiên đề đó. Đây là định nghĩa liên quan tới định lý bất toàn thứ nhất của Gödel. Không nên nhầm lẫn với sự hoàn chỉnh về mặt ngữ nghĩa với ý nghĩa là hệ tiên đề chứng minh được tất cả các hằng đúng của ngôn ngữ được nêu. Trong định lý hoàn chỉnh, Gödel đã chứng minh rằng logic bậc nhất là hoàn chỉnh về mặt ngữ nghĩa. Nhưng nó không hoàn chỉnh về mặt cú pháp, bởi vì có rất nhiều mệnh đề có thể diễn đạt trong ngôn ngữ của logic bậc nhất lại không thể được chứng minh hay không được chứng minh chỉ từ các tiên đề của logic.

Trong một hệ thống logic đơn thuần, sẽ thật vô lý nếu kỳ vọng vào sự hoàn chỉnh trong cú pháp. Nhưng trong một hệ thống toán học, những nhà tư tưởng như Hilbert tin rằng đó chỉ là vấn đề thời gian để tìm ra cách tiên đề hóa cho phép chứng minh hoặc bác bỏ (bằng cách chứng minh phủ định của nó) mọi công thức toán học.

Một hệ thống hình thức có thể không hoàn chỉnh về mặt cú pháp bởi thiết kế vốn dĩ của nó, chẳng hạn như là logic về mặt tổng quát. Hoặc có thể không hoàn chỉnh đơn giản là vì không phải tất cả các tiên đề cần thiết được khám phá hay thêm vào. Ví dụ, hình học Euclid với tiên đề song song là không hoàn chỉnh, bởi vì có vài mệnh đề trong hình học này không thể chứng minh bằng các tiên đề đang tồn tại. Tương tự như vậy, lý thuyết về thứ tự tuyến tính dày đặc không hoàn chỉnh, nhưng trở nên hoàn chỉnh với một tiên đề bổ sung cho rằng sẽ không có điểm kết thúc trong thứ tự này. Giả thuyết continuum là một mệnh đề trong ngôn ngữ của ZFC, nó không thể được chứng minh với lý thuyết này. Vì vậy, ZFC không hoàn chỉnh. Trong trường hợp này, không có một đề xuất hiển nhiên nào cho một định đề giải quyết được vấn đề.

Lý thuyết số học Peano bậc nhất dường như là nhất quán. Giả sử đúng như vậy, ta còn biết rằng nó có một tập hợp vô hạn các tiên đề nhưng lại đếm được đệ quy, và có thể mã hóa đủ lượng số học cho giả thuyết của định lý bất toàn. Vì thế, bằng định lý bất toàn thứ nhất, số học Peano là không hoàn chỉnh. Định lý đã cho một ví dụ rõ ràng về một mệnh đề của số học không thể được chứng minh hay không được chứng minh trong số học Peano. Hơn nữa, mệnh đề này là đúng trong mô hình thông thường. Thêm vào đó, không có sự mở rộng nhất quán, được tiên đề hóa một cách hiệu quả nào của số học Peano có thể là hoàn chỉnh.

Sự nhất quán

Tập hợp các tiên đề là nhất quán nếu như không có mệnh đề nào mà cả nó và phủ định của nó là chứng minh được bằng các tiên đề, và mâu thuẫn nếu ngược lại.

Sự nhất quán của số học Peano có thể chứng minh được bằng lý thuyết ZFC, nhưng không thể chứng minh được bằng chính nó. Tương tự như vậy với trường hợp của ZFC. Tuy nhiên ZFC kết hợp với "Tồn tại một số đếm không tới được" chứng minh ZFC là nhất quán bởi vì nếu κ là một số đếm nhỏ nhất thỏa mãn điều đó, thì Vκ đặt trong vũ trụ von Neumann là một mô hình của ZFC. Và một lý thuyết nhất quán khi và chỉ khi nó có một mô hình.

Nếu có một lý thuyết biến tất cả các mệnh đề trong số học Peano thành các tiên đề, thì lý thuyết đó là hoàn thiện, và có một hệ đệ quy các tiên đề và có thể mô tả phép cộng và phép nhân. Tuy nhiên, nó không nhất quán.

Một số ví dụ khác về lý thuyết không nhất quán tới từ các nghịch lý xuất hiện khi sơ đồ tiên đề bao quát không hạn chế được giả định trong lý thuyết tập hợp.